(set-option :print-success false)
(set-logic QF_UFLRA)
(set-info :status unknown)
(declare-fun P15 () Bool)
(declare-fun x5 () Real)
(declare-fun x2 () Real)
(declare-fun x22 () Real)
(declare-fun x27 () Real)
(declare-fun f0_2 (Real Real) Real)
(declare-fun x1 () Real)
(declare-fun x6 () Real)
(declare-fun P0 () Bool)
(declare-fun P19 () Bool)
(declare-fun x10 () Real)
(declare-fun x3 () Real)
(declare-fun x11 () Real)
(declare-fun x12 () Real)
(declare-fun f0_1 (Real) Real)
(declare-fun P11 () Bool)
(declare-fun x26 () Real)
(declare-fun x8 () Real)
(declare-fun x13 () Real)
(declare-fun x4 () Real)
(declare-fun P7 () Bool)
(declare-fun P25 () Bool)
(declare-fun x9 () Real)
(declare-fun x24 () Real)
(declare-fun x18 () Real)
(declare-fun x28 () Real)
(declare-fun x14 () Real)
(declare-fun P20 () Bool)
(declare-fun P29 () Bool)
(declare-fun P18 () Bool)
(declare-fun P6 () Bool)
(declare-fun x25 () Real)
(declare-fun P8 () Bool)
(declare-fun x16 () Real)
(declare-fun x19 () Real)
(declare-fun x15 () Real)
(declare-fun x29 () Real)
(declare-fun x20 () Real)
(declare-fun x23 () Real)
(declare-fun P9 () Bool)
(declare-fun x7 () Real)
(declare-fun P26 () Bool)
(declare-fun P24 () Bool)
(declare-fun P4 () Bool)
(declare-fun x17 () Real)
(declare-fun P28 () Bool)
(declare-fun x21 () Real)

(push 2)
  (assert
   (let (($x6304 (< (+ (- (* (- 3.0) x22) (* 31.0 x2)) (* 16.0 x5)) 6.0)))
   (let (($x10718 (= (f0_2 x6 x1) x27)))
   (let (($x9948 (or $x10718 $x6304)))
   (let (($x1678 (or $x9948 P15)))
   (let (($x758 (not $x1678)))
   (not $x758)))))))
  (assert
   (let (($x6973 (not P0)))
   (let (($x9585 (not P19)))
   (let (($x4166 (= (+ (* (- 12.0) x3) (* 5.0 x2) (* 24.0 x10)) 21.0)))
   (let (($x7694 (or $x4166 $x9585)))
   (let (($x6518 (or $x7694 $x6973)))
   (let (($x9249 (not $x6518)))
   (let ((?x10386 (- 1.0)))
   (let (($x8447 (< (+ (* 13.0 x12) (* 37.0 x2) (* 40.0 x11)) ?x10386)))
   (let (($x4393 (not $x8447)))
   (let ((?x9230 (f0_1 x1)))
   (let ((?x8148 (f0_1 x6)))
   (let (($x10749 (and (distinct ?x8148 ?x9230) true)))
   (let (($x10092 (or $x10749 $x4393)))
   (let (($x9476 (not $x10092)))
   (let (($x5885 (and $x9476 $x9249)))
   (not $x5885)))))))))))))))))
(check-sat)
(pop 2)

(push 2)
  (assert
   (let (($x2424 (not P11)))
   (let (($x4762 (not $x2424)))
   (not $x4762))))
  (assert
   (let (($x3659 (= (f0_2 x4 x13) (f0_2 x8 x26))))
   (and P7 $x3659)))
(check-sat)
(pop 0)

(push 2)
  (assert
   (let (($x10930 (not P25)))
   (let (($x760 (= (f0_2 x22 x24) x9)))
   (let (($x9800 (and $x760 $x10930)))
   (let (($x6501 (not $x9800)))
   (let (($x10917 (not P15)))
   (let (($x8490 (and (distinct (f0_2 x14 x28) (f0_2 x3 x18)) true)))
   (let (($x2122 (not $x8490)))
   (let (($x1855 (or P20 $x2122)))
   (let (($x10633 (and $x1855 $x10917)))
   (let (($x10860 (and $x10633 $x6501)))
   (not $x10860))))))))))))
  (assert
   (let ((?x1393 (f0_1 x8)))
   (let (($x7452 (= ?x1393 (f0_1 x9))))
   (let (($x6304 (< (+ (- (* (- 3.0) x22) (* 31.0 x2)) (* 16.0 x5)) 6.0)))
   (let (($x7218 (not $x6304)))
   (let (($x10375 (or $x7218 $x7452)))
   (and P29 $x10375)))))))
(check-sat)
(pop 2)

(push 2)
  (assert
   (not P18))
  (assert
   (let ((?x9230 (f0_1 x1)))
   (let ((?x8148 (f0_1 x6)))
   (let (($x10749 (and (distinct ?x8148 ?x9230) true)))
   (or P6 $x10749)))))
(check-sat)
(pop 0)

(push 2)
  (assert
   (let (($x611 (< (+ (* 19.0 x25) (* 29.0 x4) (* 27.0 x11)) 18.0)))
   (or $x611 P19)))
  (assert
   (let (($x7838 (not P8)))
   (let ((?x8148 (f0_1 x6)))
   (let (($x4459 (and (distinct ?x8148 (f0_2 x27 x16)) true)))
   (let (($x5872 (or $x4459 P15)))
   (let (($x3982 (and (distinct (f0_2 x4 x19) x19) true)))
   (let (($x6890 (and $x3982 $x5872)))
   (let (($x5832 (and $x6890 $x7838)))
   (not $x5832)))))))))
(check-sat)
(pop 0)

(push 2)
  (assert
   (let ((?x7869 (- 7.0)))
   (let (($x5792 (<= (- (* (- 32.0) x29) (* 11.0 x15)) ?x7869)))
   (let (($x9585 (not P19)))
   (let (($x854 (not $x9585)))
   (let (($x351 (and $x854 $x5792)))
   (not $x351)))))))
  (assert
   (let ((?x10386 (- 1.0)))
   (let (($x8447 (< (+ (* 13.0 x12) (* 37.0 x2) (* 40.0 x11)) ?x10386)))
   (let (($x984 (and (distinct (f0_1 x25) x14) true)))
   (let (($x8670 (not $x984)))
   (let (($x6007 (or $x8670 $x8447)))
   (not (not $x6007))))))))
(check-sat)
(pop 2)

(push 2)
  (assert
   (let (($x9736 (< (- (- (* (- 36.0) x20) (* 32.0 x26)) (* 29.0 x12)) 23.0)))
   (let (($x3872 (not $x9736)))
   (not $x3872))))
  (assert
   (let (($x5384 (= (f0_2 x2 x23) (f0_2 x15 x25))))
   (let (($x1021 (not $x5384)))
   (or P9 $x1021))))
(check-sat)
(pop 1)

(push 2)
  (assert
   (let (($x5384 (= (f0_2 x2 x23) (f0_2 x15 x25))))
   (let (($x1574 (not P18)))
   (let (($x9066 (< (+ (* (- 35.0) x6) (* 17.0 x7) (* 26.0 x20)) 5.0)))
   (let (($x6299 (or $x9066 $x1574)))
   (let (($x866 (and $x6299 $x5384)))
   (not $x866)))))))
  (assert
   (let ((?x194 (f0_1 x29)))
   (let (($x5627 (= ?x194 x27)))
   (let (($x3721 (not $x5627)))
   (let (($x409 (= (- (- (* (- 6.0) x29) (* 40.0 x11)) (* 27.0 x3)) 36.0)))
   (let (($x9756 (not $x409)))
   (let (($x2424 (not P11)))
   (let (($x5384 (= (f0_2 x2 x23) (f0_2 x15 x25))))
   (let (($x8249 (or $x5384 $x2424)))
   (let (($x821 (or $x8249 $x9756)))
   (and $x821 $x3721)))))))))))
(check-sat)
(pop 0)

(push 2)
  (assert
   (let (($x10303 (not P26)))
   (let (($x2431 (and (distinct (+ (- (* (- 19.0) x24) (* 19.0 x26)) x18) 21.0) true)))
   (let (($x3159 (not $x2431)))
   (or $x3159 $x10303)))))
  (assert
   (let ((?x10386 (- 1.0)))
   (< (+ (* 13.0 x12) (* 37.0 x2) (* 40.0 x11)) ?x10386)))
(check-sat)
(pop 0)

(push 2)
  (assert
   (let (($x7079 (= x22 x6)))
   (let (($x2813 (= x5 (f0_1 x12))))
   (let (($x3418 (not $x2813)))
   (let ((?x194 (f0_1 x29)))
   (let (($x11016 (= ?x194 x13)))
   (let (($x6448 (not $x11016)))
   (let (($x10199 (or $x6448 $x3418)))
   (let (($x8592 (or $x10199 $x7079)))
   (let (($x2158 (and P26 $x8592)))
   (not $x2158)))))))))))
  (assert
   (let (($x5220 (not P24)))
   (not $x5220)))
(check-sat)
(pop 2)

(push 2)
  (assert
   (let (($x2424 (not P11)))
   (let (($x8657 (not P4)))
   (let (($x10154 (or $x8657 $x2424)))
   (let (($x611 (< (+ (* 19.0 x25) (* 29.0 x4) (* 27.0 x11)) 18.0)))
   (let (($x1554 (not $x611)))
   (let (($x2079 (= (f0_2 x13 x22) (f0_1 x3))))
   (let (($x5863 (not $x2079)))
   (let (($x6223 (or P7 $x5863)))
   (let (($x4174 (or $x6223 $x1554)))
   (and $x4174 $x10154)))))))))))
  (assert
   (let (($x409 (= (- (- (* (- 6.0) x29) (* 40.0 x11)) (* 27.0 x3)) 36.0)))
   (let (($x9756 (not $x409)))
   (let ((?x9230 (f0_1 x1)))
   (let ((?x8148 (f0_1 x6)))
   (let (($x10749 (and (distinct ?x8148 ?x9230) true)))
   (let (($x4717 (or P6 $x10749)))
   (let (($x2490 (or $x4717 $x9756)))
   (not (not $x2490))))))))))
(check-sat)
(pop 1)

(push 2)
  (assert
   (let (($x7087 (and (distinct x8 x26) true)))
   (not $x7087)))
  (assert
   (let (($x984 (and (distinct (f0_1 x25) x14) true)))
   (let (($x8670 (not $x984)))
   (let (($x3786 (and $x8670 P8)))
   (not $x3786)))))
(check-sat)
(pop 0)

(push 2)
  (assert
   (let (($x5221 (and (distinct (- (+ (* 41.0 x26) (* 5.0 x13)) (* 8.0 x23)) 39.0) true)))
   (let ((?x1393 (f0_1 x8)))
   (let (($x7452 (= ?x1393 (f0_1 x9))))
   (let (($x8488 (not $x7452)))
   (let (($x7520 (and $x8488 $x5221)))
   (not $x7520)))))))
  (assert
   (let (($x7947 (<= (- (- (* (- 26.0) x22) (* 3.0 x17)) (* 22.0 x10)) 16.0)))
   (not $x7947)))
(check-sat)
(pop 0)

(push 2)
  (assert
   (let (($x3121 (not P28)))
   (let (($x6958 (not $x3121)))
   (not $x6958))))
  (assert
   (let ((?x9320 (f0_1 x21)))
   (let (($x7071 (and (distinct ?x9320 x21) true)))
   (let ((?x7869 (- 7.0)))
   (let (($x5792 (<= (- (* (- 32.0) x29) (* 11.0 x15)) ?x7869)))
   (let (($x1500 (or $x5792 $x7071)))
   (let (($x5008 (or $x1500 P0)))
   (not $x5008))))))))
(check-sat)
